$\forall$$T$:Type, ${\it eq}$:EqDecider($T$), ${\it es}$:ES, $x$:Id, $e$, ${\it e'}$:E.
\\[0ex]@loc(${\it e'}$)($x$:$T$)
\\[0ex]$\Rightarrow$ $e$ $\leq$loc ${\it e'}$ 
\\[0ex]$\Rightarrow$ (($x$ after lastchange($x$;${\it e'}$)) = ($x$ when lastchange($x$;${\it e'}$)) $\in$ $T$)
\\[0ex]$\Rightarrow$ (($x$ when $e$) = ($x$ when ${\it e'}$) $\in$ $T$)